公理语义（Axiomatic Semantics）：一种描述程序含义的方法，不是直接给出程序“如何运行”，而是用一组公理（axioms）与推理规则来说明：如果程序执行前满足某些前置条件（precondition），那么执行后会保证某些后置条件（postcondition）。它常用于程序正确性证明，典型形式是 Hoare 三元组：{P} C {Q}。
（该术语主要用于计算机科学中的形式化语义；在更广义的“语义学”语境里还有其他分支含义。）
Axiomatic semantics helps us prove that a program is correct.
公理语义帮助我们证明一个程序是正确的。
Using axiomatic semantics, we can derive a postcondition from a given precondition and a sequence of assignments, rather than simulating the program step by step.
使用公理语义，我们可以从给定的前置条件和一系列赋值语句推导出后置条件，而不是一步步地去模拟程序运行。
/ˌæksiəˈmætɪk sɪˈmæntɪks/
axiomatic 来自 axiom（公理），词根可追溯到古希腊语 axiōma，意为“被认为值得/被认可的命题”。semantics 来自希腊语 sēmantikos，意为“与意义有关的”。合起来即“用公理与推理来刻画意义”的方法，后来在程序语言理论中固定为“公理语义”。
Select Language